Was wir jetzt tun werden, und das geht über die Sachen hinaus, die Sie gemacht haben,

dass wir uns in etwas mehr Detail um Vollständigkeit kümmern, das wird heute sein,

und dann aber auch in der Aussagenlogik um effiziente Verfahren für SAT-Solver,

also für Erfüllbarkeitschecker. Und da werden wir uns dieses DPLL-Verfahren angucken,

dass, obwohl es in gewisser Weise herzzerreißend einfach ist, Stand der Kunst ist.

Gut, aber bevor wir das tun, wollen wir uns kurz wiederholen. Wir haben als Running-Beispiel

haben wir uns die Wumpuswelt angeguckt und darüber gesprochen, wie man daraus als Mensch

Reasoning macht. Wir haben uns angeguckt, wie so ein Agent aussieht. Dieser Agent ist im

Wesentlichen gesteuert durch eine Wissensbank, denen immer alle neue Informationen hinzugefügt

werden. Dann wird darauf Inferenz gemacht, so wie wir das zum Beispiel in einem Tablos

angeguckt haben, zum Beispiel aber auch jetzt in der kommenden Woche in dem DPLL.

Und wir hatten uns die Grundlagen angeguckt, Syntax, Semantik, Folgerung, Vollständigkeit

und Korrektheit eines Kalküls. Und wir hatten uns ein wenig die Anwendungen angeguckt und

es ist so, dass man sehr viele Probleme in Aussagenlogik kodieren kann. Also, das ist

Stand der Kunst, so was wie Planungsprobleme in riesige aussagenlogische Formeln zu transformieren,

die dann einem Satz-Server zum Fressen geben und der gibt dann eine Variabelbelegung zurück

oder aber auch eine Meldung, dass es unerfüllbar ist. Und dann kann man daraus, wenn es erfüllbar

ist, den Plan ablesen und wenn es unerfüllbar ist, dann muss man halt irgendwie sich überlegen,

was man stattdessen tun kann, weil das Problem unbesreit ist.

Gut, also wir haben angefangen Aussagenlogik formal zu betrachten, formal immer aus zwei

Arten, einmal wie kann man in der Aussagenlogik Inferenz machen und zum anderen, was sind

die Eigenschaften der Kalkülse. Beides werden wir heute sehen. Die Syntax ist sehr einfach,

wir haben Aussagenvariabeln, wir haben Junktoren und wir bauen aus den Aussagenvariablen und

den Junktoren bauen wir Formeln auf, das sind relativ einfache Gebilde. Ich habe da ein

paar Beispiele, haben wir durchgesprochen. Wir können der ganzen Sache eine Semantik

geben, auch in der absolut offensichtlichen Art und Weise, Sie haben das alle schon gesehen.

Wir haben ein festes Modell, war und falsch, wir haben Variabelbelegungen, Phi, Psi und

so weiter und so fort und wir rechnen den Wert einer Formel unter einer Belegung in

diesem einen festen Modell im Wesentlichen dadurch aus, dass wir das als einen Homomorphismus

sehen. Das heißt, wir können die Berechnung runterziehen, rekursiv bis auf Variablenebene,

dort schlägt die Variabelbelegung zu und dann kann man die Werte wieder hoch propagieren,

wenn man dann irgendwann einen Wert einer Formel hat. So würden wir es programmieren,

als Menschen machen wir es anders, als Menschen machen wir es mehr wahrheitstabell. Wir interessieren

uns insgesamt für die semantischen Eigenschaften von Formeln, insbesondere für eine besondere,

nämlich die Allgemeingültigkeit. Allgemeingültigkeit heißt, dass diese Formel in allen Modellen,

das ist trivial, wir haben nur eins, unter allen Belegungen wahr wird. Das heißt, wir

kriegen den Wert unter dieser Belegung als wahr und dann bezeichnen wir solche Formel

als allgemeingültig, valid im Englischen und wir haben eine duale Form, das ist die Unerfüllbarkeit,

die benutzen wir immer dann, wenn wir eine Negation im Spiel haben und zwar ist es eine

Formel, ist allgemeingültig, wenn ihre Negation unerfüllbar ist und dann haben wir noch zwei

wesentlichen Fehlerfälle. Wir haben einmal die Erfüllbarkeit, das ist nämlich nicht

unerfüllbar und wir haben die Falsifizierbarkeit als nicht allgemeingültig. Das sind so die

Normalfälle. Wir haben die Folgerung angeguckt und haben das Ganze dann auf die Wumpuswelt,

nein, das haben wir glaube ich nicht, die Formel hatte ich gesucht und dann hinterher

nicht gefunden. Wenn wir jetzt diese Logik mit der Bedeutung, die wir ihr gegeben haben,

anwenden wollen, ich hätte gesagt, dass man sehr viele Probleme in Aussagenlogik reinkodieren

kann, in diesem Fall hier die Wumpuswelt auch und da kann man jetzt diese Regeln, die wir

haben, kann man einfach in Aussagenlogische Variablen kodieren. Wir haben sozusagen zwei

Arten in dieser Kodierung, wir haben zwei Arten von Aussagenlogischen Variablen. Wir haben

die W I J, das sagt gerade der Wumpus ist in Zelle I und J und dann haben wir es stinkt,